Inference at * 
Iof proof for Lemma p-inject wf:


  A, B:Type, f:(A(B + Top)). p-inject(A;B;f)   

latex

 by (Unfold `p-inject` ( 0)) 
CollapseTHEN (Auto) 

latex

C.

Definitions	p-inject(A;B;f), b, can-apply(f;x), suptype(S; T), do-apply(f;x), P  Q, , s = t, S  T, x:A. B(x), x:A.B(x), Void, x:AB(x), left + right, Top, t  T, Type
Lemmas	assert wf, can-apply wf, do-apply wf, top wf